1. Technical Field
The present invention relates generally to managing model checks of sequential designs, and in particular, to a computer implemented method for utilizing the cached results of prior model checking runs in a centralized persistent database.
2. Description of Related Art
As circuits have become more complex, improved methods and tools for designing, modifying, and testing those circuits have been developed. Circuits can include integrated circuits, printed circuit board circuits, and other types of circuits at a system level, sub-system level, or even at a transistor level. Improvements in circuit design include the use of electronic design automation (EDA) software tools to generate schematics of circuit designs between a logic and physical design.
Circuit designers need to test or otherwise verify their circuit designs before actually constructing a circuit from a design. A variety of software testing tools and techniques have been developed for testing circuit designs including simulation and formal verification. While simulation can be very effective, it can become very time consuming and may not be able to exhaustively test complex circuit designs due to the large number of possible test vectors, input bits and state bits used to simulate a given circuit. However, formal verification of a circuit design can be helpful in proving the correctness of those circuit designs.
Model checking is a type of formal verification where a model of a circuit design is exhaustively checked to determine whether that model meets a set of specifications. The circuit design is first compiled into a formal netlist. This formal netlist is commonly represented as a directed-acyclic graph (DAG) where nodes typically represent user and internal variables as well as operators (e.g. Boolean AND), and where edges connect the nodes (operands) to the operators. The model checking system then attempts all possible input combinations and circuit states for that model given a reset state and a property signal. All possible reachable circuit states are then mathematically identified and checked to verify that the model meets the set of specifications. Powerful Boolean engines may be utilized to assist in this process. However, a model check of a complex circuit design may take hours to run. If a circuit designer iteratively makes circuit design changes, then the circuit design iterations may need to be model checked, thereby slowing the circuit design process.